(0) Obligation:

Clauses:

gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: gopher(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

gopherA(.(.(X1, X2), X3), X4) :- gopherA(cons(X1, cons(X2, X3)), X4).
gopherA(.(.(X1, X2), X3), X4) :- gopherA(cons(X1, cons(X2, X3)), X4).

Clauses:

gophercA(nil, nil).
gophercA(.(nil, X1), cons(nil, X1)).
gophercA(.(.(X1, X2), X3), X4) :- gophercA(cons(X1, cons(X2, X3)), X4).
gophercA(.(.(X1, X2), X3), X4) :- gophercA(cons(X1, cons(X2, X3)), X4).

Afs:

gopherA(x1, x2)  =  gopherA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
gopherA_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → U1_GA(X1, X2, X3, X4, gopherA_in_ga(cons(X1, cons(X2, X3)), X4))
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → GOPHERA_IN_GA(cons(X1, cons(X2, X3)), X4)

R is empty.
The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2)  =  gopherA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
cons(x1, x2)  =  cons(x1, x2)
GOPHERA_IN_GA(x1, x2)  =  GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → U1_GA(X1, X2, X3, X4, gopherA_in_ga(cons(X1, cons(X2, X3)), X4))
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → GOPHERA_IN_GA(cons(X1, cons(X2, X3)), X4)

R is empty.
The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2)  =  gopherA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
cons(x1, x2)  =  cons(x1, x2)
GOPHERA_IN_GA(x1, x2)  =  GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 2 less nodes.

(6) TRUE